ds:(IdType), da:(IdKndType), A:Type, X:Interface(ds;da;A).
interface-inl(X)  Interface(ds;da;{x:A + Top| isl(x)} ) 

latex

Definitions	Top, t  T, left + right, f(a), x:AB(x), Type, x:A  B(x), a:A fp B(a), Atom$n, Id, Knd, let x,y = A in B(x;y), True, b, inl x , x:A. B(x), isl(x), , Unit, ff, tt, False, case b of inl(x) => s(x) | inr(y) => t(y), {x:A| B(x)} , x.A(x), f o g  , let i,k:LocKnd = ik in P(i;k), LocKnd, hasloc(k;i), x,y. t(x;y), (x  l), type List, x:A.B(x), x. t(x), g o f, interface-inl(X), Interface(ds;da;A)
Lemmas	fpf-compose wf, l member wf, LocKnd wf, locknd-spread wf2, hasloc wf, Knd wf, Id wf, p-compose wf, true wf, false wf, btrue wf, bfalse wf, assert wf, isl wf, top wf